f, g:x:Id fp Type, x:Id. (x  dom(f  g))  ((x  dom(f))  (x  dom(g))) 

latex

Definitions	x:A. B(x), t  T, x. t(x), P  Q, P  Q, P  Q, , P  Q, P & Q, x(s)
Lemmas	Id wf, fpf wf, iff functionality wrt iff, assert wf, fpf-dom wf, id-deq wf, fpf-join wf, top wf, fpf-trivial-subtype-top, fpf-join-dom